ecl-es-halt(es;x)
== ecl_ind(x;k,test.n,e1,e2. if n=0 e2 = first e  e1.kind(e) = k & test((state when e),val(e))
== ecl_ind(x;k,test.n,e1,e2. else False fi;a,b,ha,hb.n,e1,e2. if n=0 False else ha(n,e1,e2) fi
==  e(e1,e2].ha(0,e1,pred(e)) & hb(n,e,e2);a,b,ha,hb.n,e1,e2.
== if n=0 ha(0,e1,e2) & e[e1,e2].hb(0,e1,e)  hb(0,e1,e2) & e[e1,e2].ha(0,e1,e)
== else ha(n,e1,e2) & m0.ecl-ex(b).if nm e[e1,e2).hb(m,e1,e) else e[e1,e2].hb(m,e1,e) fi
== else  hb(n,e1,e2)
== else  & m0.ecl-ex(a).
== else  & if nm e[e1,e2).ha(m,e1,e) else e[e1,e2].ha(m,e1,e) fi fi;a,b,ha,hb.n,e1,e2.
== ha(n,e1,e2) & m0.ecl-ex(b).if nm e[e1,e2).hb(m,e1,e) else e[e1,e2].hb(m,e1,e) fi
==  hb(n,e1,e2)
==  & m0.ecl-ex(a).if nm e[e1,e2).ha(m,e1,e) else e[e1,e2].ha(m,e1,e) fi;a,ha.n,e1,e2.
== if n=0 False else [e1;e2]~([x,y].ha(0,x,y))*[x,y].ha(n,x,y) fi;a,m,ha.ha;a,m,ha.n,e1,e2.
== if n=0 False else ha(n,e1,e2) fi  if n=m ha(0,e1,e2) else False fi;a,l,ha.n,e1,e2. ha
== if n=0 False else ha(n,e1,e2) fi  if n=m ha(0,e1,e2) else False fi;a,l,ha.n,e1,e2. (n
== if n=0 False else ha(n,e1,e2) fi  if n=m ha(0,e1,e2) else False fi;a,l,ha.n,e1,e2. ,e1
== if n=0 False else ha(n,e1,e2) fi  if n=m ha(0,e1,e2) else False fi;a,l,ha.n,e1,e2. ,e2)
== & (n  l)
==  if n=0 (ml.ha(m,e1,e2)) else False fi) 

latex

---

clarification:

ecl-es-halt(es;x)
== ecl_ind(x;k,test.n,e1,e2. if n=0
== ecl_ind(x;k,test.n,e1,e2. if es-first-since(es;e.es-kind(es; e) = k  Knd
== ecl_ind(x;k,test.n,e1,e2. if & test(es-state-when(es;e),es-val(es; e));e1;e2)
== ecl_ind(x;k,test.n,e1,e2. else False fi;a,b,ha,hb.n,e1,e2. if n=0 False else ha(n,e1,e2) fi
==  existse-between3(es;e1;e2;e.ha(0,e1,es-pred(es; e)) & hb(n,e,e2));a,b,ha,hb.n,e1,e2.
== if n=0
== if ha(0,e1,e2) & existse-between2(es;e1;e2;e.hb(0,e1,e))
== if  hb(0,e1,e2) & existse-between2(es;e1;e2;e.ha(0,e1,e))
== else ha(n,e1,e2)
== else & m0.ecl-ex(b).
== else & if nm alle-between1(es;e1;e2;e.hb(m,e1,e))
== else & else alle-between2(es;e1;e2;e.hb(m,e1,e)) fi
== else  hb(n,e1,e2)
== else  & m0.ecl-ex(a).
== else  & if nm alle-between1(es;e1;e2;e.ha(m,e1,e))
== else  & else alle-between2(es;e1;e2;e.ha(m,e1,e)) fi fi;a,b,ha,hb.n,e1,e2. ha(n,e1,e2)
== & m0.ecl-ex(b).
== & if nm alle-between1(es;e1;e2;e.hb(m,e1,e)) else alle-between2(es;e1;e2;e.hb(m,e1,e)) fi
==  hb(n,e1,e2)
==  & m0.ecl-ex(a).
==  & if nm alle-between1(es;e1;e2;e.ha(m,e1,e))
==  & else alle-between2(es;e1;e2;e.ha(m,e1,e)) fi;a,ha.n,e1,e2.
== if n=0 False
== else es-pstar-q(es;x,y.ha(0,x,y);x,y.ha(n,x,y);e1;e2) fi;a,m,ha.ha;a,m,ha.n,e1,e2. if n=0
== else es-pstar-q(es;x,y.ha(0,x,y);x,y.ha(n,x,y);e1;e2) fi;a,m,ha.ha;a,m,ha.n,e1,e2. if False
== else es-pstar-q(es;x,y.ha(0,x,y);x,y.ha(n,x,y);e1;e2) fi;a,m,ha.ha;a,m,ha.n,e1,e2. else ha
== else es-pstar-q(es;x,y.ha(0,x,y);x,y.ha(n,x,y);e1;e2) fi;a,m,ha.ha;a,m,ha.n,e1,e2. else (n
== else es-pstar-q(es;x,y.ha(0,x,y);x,y.ha(n,x,y);e1;e2) fi;a,m,ha.ha;a,m,ha.n,e1,e2. else ,e1
== else es-pstar-q(es;x,y.ha(0,x,y);x,y.ha(n,x,y);e1;e2) fi;a,m,ha.ha;a,m,ha.n,e1,e2. else ,e2) fi
==  if n=m ha(0,e1,e2) else False fi;a,l,ha.n,e1,e2. ha(n,e1,e2) & (n  l  )
==  if n=0 l_exists(l;;m.ha(m,e1,e2)) else False fi) 

latex

Definitions	ecl ind, e2 = first e  e1.P(e), A & B, s = t, Knd, kind(e), b, (state when e), val(e), e(e1,e2].P(e), pred(e), e[e1,e2].P(e), xL.P(x), car.cdr, ecl-ex(x), ij, e[e1,e2).P(e), e[e1,e2].P(e), [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), x.A(x), P  Q, P & Q, A, (x  l), if b t else f fi, i=j, #$n, (xL.P(x)), , f(a), False
FDL editor aliases	ecl-es-halt